$\forall$$i$, $x$:Id, $T$:Type, $v$:$T$, $A$:Realizer. $\neg$R{-}occurs($A$;$i$;$x$) $\Rightarrow$ @$i$ $x$ initially $v$:$T$ $\parallel$ $A$